Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		from(X)	→ cons(X,n__from(n__s(X)))
2:		head(cons(X,XS))	→ X
3:		2nd(cons(X,XS))	→ head(activate(XS))
4:		take(0,XS)	→ nil
5:		take(s(N),cons(X,XS))	→ cons(X,n__take(N,activate(XS)))
6:		sel(0,cons(X,XS))	→ X
7:		sel(s(N),cons(X,XS))	→ sel(N,activate(XS))
8:		from(X)	→ n__from(X)
9:		s(X)	→ n__s(X)
10:		take(X1,X2)	→ n__take(X1,X2)
11:		activate(n__from(X))	→ from(activate(X))
12:		activate(n__s(X))	→ s(activate(X))
13:		activate(n__take(X1,X2))	→ take(activate(X1),activate(X2))
14:		activate(X)	→ X

There are 12 dependency pairs:


15:		2nd#(cons(X,XS))	→ HEAD(activate(XS))
16:		2nd#(cons(X,XS))	→ ACTIVATE(XS)
17:		TAKE(s(N),cons(X,XS))	→ ACTIVATE(XS)
18:		SEL(s(N),cons(X,XS))	→ SEL(N,activate(XS))
19:		SEL(s(N),cons(X,XS))	→ ACTIVATE(XS)
20:		ACTIVATE(n__from(X))	→ FROM(activate(X))
21:		ACTIVATE(n__from(X))	→ ACTIVATE(X)
22:		ACTIVATE(n__s(X))	→ S(activate(X))
23:		ACTIVATE(n__s(X))	→ ACTIVATE(X)
24:		ACTIVATE(n__take(X1,X2))	→ TAKE(activate(X1),activate(X2))
25:		ACTIVATE(n__take(X1,X2))	→ ACTIVATE(X1)
26:		ACTIVATE(n__take(X1,X2))	→ ACTIVATE(X2)

The approximated dependency graph contains 2 SCCs: {17,21,23-26} and {18}.

Consider the SCC {17,21,23-26}. The usable rules are {1,4,5,8-14}. The constraints could not be solved.

Consider the SCC {18}. The usable rules are {1,4,5,8-14}. By taking the AF π with π(n__take) = π(SEL) = π(take) = 1, π(cons) = 2 and π(from) = π(n__from) = [ ] together with the lexicographic path order with precedence 0 ≻ nil, activate ≻ from ≻ n__from and activate ≻ s ≻ n__s, the rules in {10,13} are weakly decreasing and the rules in {1,4,5,8,9,11,12,14,18} are strictly decreasing.

Tyrolean Termination Tool (0.96 seconds) --- May 3, 2006